PRISM
=====
Version: 4.5
Date: Wed Apr 01 08:00:01 UTC 2020
Hostname: cb4ac6bf600d
Memory limits: cudd=1g, java(heap)=2g
Type: CTMC
Modules: S1_def S2_def S3_def S4_def Y_def Z_def CC_def XX_def
Variables: S1 S2 S3 S4 Y Z CC XX
Generator: stamina.InfCTMCModelGenerator
Type: CTMC
========================================================================
Approximation<1> : kappa = 1.0E-6
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 20261 21964 22704 23102 23194 states
1 23194 states
Reachable states exploration and model construction done in 14.1 secs.
Sorting reachable states list...
Time for model construction: 14.189 seconds.
Type: CTMC
States: 23194 (1 initial)
Transitions: 234255
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((S2>80&(!S2=-1))&(S3<20&(!S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.07891393689045 x 2100.0 = 4365.719267469945
Fox-Glynn (1.25E-7): left = 3900, right = 4928
Backwards transient probability computation took 4929 iters and 42.295 seconds.
Value in the initial state: 0.0
Time for model checking: 42.343 seconds.
Result: 0.0 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((S2>80|(S2=-1))&(S3<20|(S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.07891393689045 x 2100.0 = 4365.719267469945
Fox-Glynn (1.25E-7): left = 3900, right = 4928
Backwards transient probability computation took 4929 iters and 42.853 seconds.
Value in the initial state: 0.09686551359515974
Time for model checking: 42.873 seconds.
Result: 0.09686551359515974 (value in the initial state)
========================================================================
Approximation<2> : kappa = 9.999999999999999E-10
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 92572 127772 143277 155694 161974 167387 170961 173675 175848 177369 178809 179784 180940 181667 182462 183042 183632 184175 184562 184987 185293 185662 185908 186131 186348 186528 186744 186891 187121 187226 187331 187446 187585 187667 187725 187802 states
1 128802 187802 states
Reachable states exploration and model construction done in 112.344 secs.
Sorting reachable states list...
Time for model construction: 113.144 seconds.
Type: CTMC
States: 187802 (1 initial)
Transitions: 2122923
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((S2>80&(!S2=-1))&(S3<20&(!S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.1904732333728623 x 2100.0 = 4599.993790083011
Fox-Glynn (1.25E-7): left = 4122, right = 5177
Backwards transient probability computation took 5178 iters and 377.396 seconds.
Value in the initial state: 0.041207214924721916
Time for model checking: 377.445 seconds.
Result: 0.041207214924721916 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((S2>80|(S2=-1))&(S3<20|(S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.1904732333728623 x 2100.0 = 4599.993790083011
Fox-Glynn (1.25E-7): left = 4122, right = 5177
Backwards transient probability computation took 5178 iters and 377.591 seconds.
Value in the initial state: 0.04292471670708871
Time for model checking: 377.615 seconds.
Result: 0.04292471670708871 (value in the initial state)
========================================================================
Approximation<3> : kappa = 9.999999999999998E-13
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 214138 242339 271383 306767 332644 361206 394486 409187 419177 430101 443460 450856 458489 465828 472018 474274 475110 477568 480219 482322 483735 486148 487705 490077 491689 492101 492706 493064 493536 493826 494228 494507 494741 495013 495111 495270 495343 495485 495610 495718 495833 495919 495973 496019 496080 496117 496161 496214 496262 496327 496335 states
1 108452 222618 340011 444108 496335 states
Reachable states exploration and model construction done in 165.261 secs.
Sorting reachable states list...
Time for model construction: 166.924 seconds.
Type: CTMC
States: 496335 (1 initial)
Transitions: 6176094
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((S2>80&(!S2=-1))&(S3<20&(!S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.235211012497352 x 2100.0 = 4693.94312624444
Fox-Glynn (1.25E-7): left = 4211, right = 5276
Backwards transient probability computation took 5277 iters and 1091.183 seconds.
Value in the initial state: 0.04229415348240532
Time for model checking: 1091.3 seconds.
Result: 0.04229415348240532 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((S2>80|(S2=-1))&(S3<20|(S3=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 2.235211012497352 x 2100.0 = 4693.94312624444
Fox-Glynn (1.25E-7): left = 4211, right = 5276
Backwards transient probability computation took 5277 iters and 1094.664 seconds.
Value in the initial state: 0.0422946883070432
Time for model checking: 1094.725 seconds.
Result: 0.0422946883070432 (value in the initial state)
========================================================================
Property: "change_state": P=? [ F<=T ((S2>80)&(S3<20)) ]
ProbMin: 0.04229415348240532 (value in the initial state)
ProbMax: 0.0422946883070432 (value in the initial state)
========================================================================
----------
Computation aborted after 3321.3579185009003 seconds since the total time limit of 1800 seconds was exceeded.